#define N 5
#define K 3

void main() {

  bool G[N][N] = { 
     {0, 1, 0, 0, 1}, 
     {0, 0, 1, 0, 0},
     {0, 1, 0, 1, 0},
     {1, 0, 0, 0, 0},
     {0, 0, 0, 0, 1}, 
  };

  bool result1 = 1;
  int node1 = 0;

  // i = 0
  int next1 = nondet() % N;
  bool result2 = result1 && G[node1][next1];
  int node2 = next1;

  // i = 1
  int next2 = nondet() % N;
  bool result3 = result2 && G[node2][next2];
  int node3 = next2;
  
  // i = 2
  int next3 = nondet() % N;
  bool result4 = result3 && G[node3][next3];
  int node4 = next3;
   
  bool result5 = result4 && (node4 == 0) && (K > 0);
   
  assert(!result5);
}

